ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), i:Id, es:event_system{i:l}.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (e1,e2:es-E(es).
 (loc(e1) = i)
  (loc(e2) = i)
  (t:event-info(ds;da). (t  es-hist{i:l}(es;e1;e2))  e[e1,e2].t = es-info(es;e))) 

latex

Definitions

es-valtype(es; e), Kind-deq, es-kind(es; e), es-vartype(es; i; x), fpf-cap(f; eq; x; z), id-deq, top, event_system{i:l}, Knd, fpf(A; a.B(a)), P  Q, P  Q, es-hist{i:l}(es;e1;e2), P  Q, (x  l), e[e1,e2].P(e), x. t(x), prop{i:l}, event-info(ds;da), es-info(es;e), A, False, P  Q, b, es-E(es), Id, loc(e), x:A. B(x), t  T, [e, e'], sq_type(T), guard(T), x:A. B(x), A c B, es-le(es; e; e'), x:A  B(x), atom{$n:n}, x:AB(x), t.1, s = t, P  Q, {x:A| B(x)} , , a < b, ||as||, void, A  B, , es-first(es; e), sqequal(s; t), let x,y = A in B(x;y), True, T, left + right, <a, b>, l[i], #$n, ge(i; j), Type

Lemmas

length wf1, select wf, nat properties, squash wf, true wf, not wf, assert wf, es-first wf, es-le-loc, es-le wf, member-es-interval, member map, es-interval wf2, Id sq, es-loc wf, Id wf, es-E wf, es-loc-pred, es-info wf, event-info wf, existse-between2 wf, l member subtype, es-hist wf, l member wf, fpf wf, Knd wf, event system wf, top wf, id-deq wf, fpf-cap wf, es-vartype wf, es-kind wf, Kind-deq wf, es-valtype wf